es:ES, i:Id, L:IdLnk List, T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 e@i.
 n:||"table" when e|| .
 st-atom("table" when e;n) = st-atom("table" when es-init(es;e);n)  Atom1 

latex

Definitions

"$x", Prop, P  Q, Id, e@i. P(e), t  T, x:A. B(x), True, true, P  Q, x. t(x), if b t else f fi, T, i  j < k, P  Q, {i..j}, es-frame(es;i;L;x;T), false, P & Q, Top, {T}, SQType(T), es-secret-server, , @i only events in L change   x : T, A & B, let x = a in b(x), x(s), , Unit, xL. P(x), x:A. B(x), @i events of kind k change x to f State(ds) (val:T), False, AB, A, , x when e

Lemmas

secret-table wf, es-secret-server wf, es-E wf, nat wf, es-loc wf, st-length wf, Id wf, es-when wf, event system wf, IdLnk wf, int seg wf, es-vartype wf, assert of le int, iff transitivity, eqtt to assert, assert wf, bnot wf, bnot of lt int, eqff to assert, lt int wf, es-constant-1, squash wf, true wf, map wf, assert of lt int, le wf, le int wf, rcv wf, st-atom wf, bool wf, Knd wf, id-deq wf, es-kind wf, fpf-cap-single1, member map, l member wf, es-val wf, st-encrypt wf, st-length-encrypt, st-atom-encrypt, es-loc-init, es-init wf, ss-table-length